es:ES, e, e', ev:E. (ev  [e, e'])  e  ev  & ev  e'  

latex

Definitions	{T}, [e, e'], P  Q, P  Q, P  Q, filter(P;l), as @ bs, before(e), es-ble{i:l}(es;e;e'), (x  l), b, P & Q, e  e' , Prop, (e <loc e'), P  Q, False, E, x:A. B(x), t  T, ES
Lemmas	event system wf, es-E wf, false wf, es-locl wf, l member wf, assert wf, es-le wf, es-ble wf, es-before wf, append wf, filter wf, assert-es-ble, and functionality wrt iff, iff functionality wrt iff, nil member, or functionality wrt iff, cons member, member-es-before, member append, member filter